/-
Copyright (c) 2023 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/

import algebra.star.basic
import group_theory.submonoid.basic

/-! # Star ordered rings

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

We define the class `star_ordered_ring R`, which says that the order on `R` respects the
star operation, i.e. an element `r` is nonnegative iff it is in the `add_submonoid` generated by
elements of the form `star s * s`. In many cases, including all C⋆-algebras, this can be reduced to
`0 ≤ r ↔ ∃ s, r = star s * s`. However, this generality is slightly more convenient (e.g., it
allows us to register a `star_ordered_ring` instance for `ℚ`), and more closely resembles the
literature (see the seminal paper [*The positive cone in Banach algebras*][kelleyVaught1953])

In order to accodomate `non_unital_semiring R`, we actually don't characterize nonnegativity, but
rather the entire `≤` relation with `star_ordered_ring.le_iff`. However, notice that when `R` is a
`non_unital_ring`, these are equivalent (see `star_ordered_ring.nonneg_iff` and
`star_ordered_ring.of_nonneg_iff`).

## TODO

* In a Banach star algebra without a well-defined square root, the natural ordering is given by the
positive cone which is the _closure_ of the sums of elements `star r * r`. A weaker version of
`star_ordered_ring` could be defined for this case (again, see
[*The positive cone in Banach algebras*][kelleyVaught1953]). Note that the current definition has
the advantage of not requiring a topology.
-/

universe u
variable {R : Type u}

/--
An ordered `*`-ring is a ring which is both an `ordered_add_comm_group` and a `*`-ring,
and the nonnegative elements constitute precisely the `add_submonoid` generated by
elements of the form `star s * s`.

If you are working with a `non_unital_ring` and not a `non_unital_semiring`, it may be more
convenient do declare instances using `star_ordered_ring.of_nonneg_iff'`. -/
class star_ordered_ring (R : Type u) [non_unital_semiring R] [partial_order R]
  extends star_ring R :=
(add_le_add_left : ∀ a b : R, a ≤ b → ∀ c : R, c + a ≤ c + b)
(le_iff          : ∀ x y : R,
  x ≤ y ↔ ∃ p, p ∈ add_submonoid.closure (set.range $ λ s, star s * s) ∧ y = x + p)

namespace star_ordered_ring

@[priority 100] -- see note [lower instance priority]
instance to_ordered_add_comm_monoid [non_unital_semiring R] [partial_order R]
  [star_ordered_ring R] : ordered_add_comm_monoid R :=
{ ..show non_unital_semiring R, by apply_instance,
  ..show partial_order R, by apply_instance,
  ..show star_ordered_ring R, by apply_instance }

@[priority 100] -- see note [lower instance priority]
instance to_has_exists_add_of_le [non_unital_semiring R] [partial_order R]
  [star_ordered_ring R] : has_exists_add_of_le R :=
{ exists_add_of_le := λ a b h, match (le_iff _ _).mp h with ⟨p, _, hp⟩ := ⟨p, hp⟩ end }

@[priority 100] -- see note [lower instance priority]
instance to_ordered_add_comm_group [non_unital_ring R] [partial_order R] [star_ordered_ring R] :
  ordered_add_comm_group R :=
{ ..show non_unital_ring R, by apply_instance,
  ..show partial_order R, by apply_instance,
  ..show star_ordered_ring R, by apply_instance }

/-- To construct a `star_ordered_ring` instance it suffices to show that `x ≤ y` if and only if
`y = x + star s * s` for some `s : R`.

This is provided for convenience because it holds in some common scenarios (e.g.,`ℝ≥0`, `C(X, ℝ≥0)`)
and obviates the hassle of `add_submonoid.closure_induction` when creating those instances.

If you are working with a `non_unital_ring` and not a `non_unital_semiring`, see
`star_ordered_ring.of_nonneg_iff` for a more convenient version. -/
@[reducible] -- set note [reducible non-instances]
def of_le_iff [non_unital_semiring R] [partial_order R] [star_ring R]
  (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
  (h_le_iff : ∀ x y : R, x ≤ y ↔ ∃ s, y = x + star s * s) :
  star_ordered_ring R :=
{ add_le_add_left := @h_add,
  le_iff := λ x y,
  begin
    refine ⟨λ h, _, _⟩,
    { obtain ⟨p, hp⟩ := (h_le_iff x y).mp h,
      exact ⟨star p * p, add_submonoid.subset_closure ⟨p, rfl⟩, hp⟩ },
    { rintro ⟨p, hp, hpxy⟩,
      revert x y hpxy,
      refine add_submonoid.closure_induction hp _ (λ x y h, add_zero x ▸ h.ge) _,
      { rintro _ ⟨s, rfl⟩ x y rfl,
        nth_rewrite 0 [←add_zero x],
        refine h_add _ x,
        exact (h_le_iff _ _).mpr ⟨s, by rw [zero_add]⟩ },
      { rintro a b ha hb x y rfl,
        nth_rewrite 0 [←add_zero x],
        refine h_add ((ha 0 _ (zero_add a).symm).trans (hb a _ rfl)) x } }
  end,
  .. ‹star_ring R› }

/-- When `R` is a non-unital ring, to construct a `star_ordered_ring` instance it suffices to
show that the nonnegative elements are precisely those elements in the `add_submonoid` generated
by `star s * s` for `s : R`. -/
@[reducible] -- set note [reducible non-instances]
def of_nonneg_iff [non_unital_ring R] [partial_order R] [star_ring R]
  (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
  (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ x ∈ add_submonoid.closure (set.range $ λ s : R, star s * s)) :
  star_ordered_ring R :=
{ add_le_add_left := @h_add,
  le_iff := λ x y,
    begin
      haveI : covariant_class R R (+) (≤) := ⟨λ _ _ _ h, h_add h _⟩,
      simpa only [←sub_eq_iff_eq_add', sub_nonneg, exists_eq_right'] using h_nonneg_iff (y - x),
    end,
  .. ‹star_ring R› }

/-- When `R` is a non-unital ring, to construct a `star_ordered_ring` instance it suffices to
show that the nonnegative elements are precisely those elements of the form `star s * s`
for `s : R`.

This is provided for convenience because it holds in many common scenarios (e.g.,`ℝ`, `ℂ`, or
any C⋆-algebra), and obviates the hassle of `add_submonoid.closure_induction` when creating those
instances. -/
@[reducible] -- set note [reducible non-instances]
def of_nonneg_iff' [non_unital_ring R] [partial_order R] [star_ring R]
  (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
  (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ ∃ s, x = star s * s) :
  star_ordered_ring R :=
of_le_iff @h_add
begin
  haveI : covariant_class R R (+) (≤) := ⟨λ _ _ _ h, h_add h _⟩,
  simpa [sub_eq_iff_eq_add', sub_nonneg] using λ x y, h_nonneg_iff (y - x),
end

lemma nonneg_iff [non_unital_semiring R] [partial_order R] [star_ordered_ring R]
  {x : R} : 0 ≤ x ↔ x ∈ add_submonoid.closure (set.range $ λ s : R, star s * s) :=
by simp only [le_iff, zero_add, exists_eq_right']

end star_ordered_ring

section non_unital_semiring

variables [non_unital_semiring R] [partial_order R] [star_ordered_ring R]

lemma star_mul_self_nonneg (r : R) : 0 ≤ star r * r :=
star_ordered_ring.nonneg_iff.mpr $ add_submonoid.subset_closure ⟨r, rfl⟩

lemma star_mul_self_nonneg' (r : R) : 0 ≤ r * star r :=
by { nth_rewrite_rhs 0 [←star_star r], exact star_mul_self_nonneg (star r) }

lemma conjugate_nonneg {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ star c * a * c :=
begin
  rw star_ordered_ring.nonneg_iff at ha,
  refine add_submonoid.closure_induction ha (λ x hx, _) (by rw [mul_zero, zero_mul])
    (λ x y hx hy, _),
  { obtain ⟨x, rfl⟩ := hx,
    convert star_mul_self_nonneg (x * c) using 1,
    rw [star_mul, ←mul_assoc, mul_assoc _ _ c] },
  { calc 0 ≤ star c * x * c + 0 : by rw [add_zero]; exact hx
     ...   ≤ star c * x * c + star c * y * c : star_ordered_ring.add_le_add_left _ _ hy _
     ...   ≤ _ : by rw [mul_add, add_mul] }
end

lemma conjugate_nonneg' {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ c * a * star c :=
by simpa only [star_star] using conjugate_nonneg ha (star c)

lemma conjugate_le_conjugate {a b : R} (hab : a ≤ b) (c : R) : star c * a * c ≤ star c * b * c :=
begin
  rw [star_ordered_ring.le_iff] at hab ⊢,
  obtain ⟨p, hp, rfl⟩ := hab,
  simp_rw [←star_ordered_ring.nonneg_iff] at hp ⊢,
  exact ⟨star c * p * c, conjugate_nonneg hp c, by simp only [add_mul, mul_add]⟩,
end

lemma conjugate_le_conjugate' {a b : R} (hab : a ≤ b) (c : R) : c * a * star c ≤ c * b * star c :=
by simpa only [star_star] using conjugate_le_conjugate hab (star c)

end non_unital_semiring
